Nuprl Lemma : qless_irreflexivity
11,40
postcript
pdf
a
:rationals. qless(
a
;
a
)
False
latex
Definitions
x
:
A
.
B
(
x
)
,
x
:
A
B
(
x
)
Lemmas
qless
irreflexivity
qorder
origin
a:rationals. qless(a; a) 
False a:rationals. qless(a; a) False x:A. B(x)
B(x)